(set-option :global-decls false)
(set-option :smt.mbqi false)
(set-option :auto_config false)
(set-option :smt.arith.nl false)

(declare-sort Term)

(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun t () Int)
(declare-fun z () Int)
(declare-fun f (Int) Int)
(declare-fun _add (Int Int) Int)
(declare-fun _mul (Int Int) Int)
(declare-fun _div (Int Int) Int)

(assert (= a z))
(assert (= t 3))
(assert (forall ((x Int) (y Int)) (! (= (_add x y) (+ x y)) :pattern ((_add x y)))))
(assert (forall ((x Int) (y Int)) (! (= (_mul x y) (* x y)) :pattern ((_mul x y)))))
(assert (forall ((x Int) (y Int)) (! (= (_div x y) (div x y)) :pattern ((_div x y)))))

(declare-fun A () Term)
(declare-fun B () Term)
(declare-fun C () Term)
(declare-fun T () Term)
(declare-fun Z () Term)
(declare-fun F (Term) Term)
(declare-fun _Add (Term Term) Term)
(declare-fun _Mul (Term Term) Term)
(declare-fun _Div (Term Term) Term)
(declare-fun box (Int) Term)
(declare-fun unbox (Term) Int)

(assert (= A Z))
(assert (= T (box 3)))
(assert (forall ((x Term) (y Term)) (! (= (_Add x y) (box (+ (unbox x) (unbox y)))) :pattern ((_Add x y)))))
(assert (forall ((x Term) (y Term)) (! (= (_Mul x y) (box (* (unbox x) (unbox y)))) :pattern ((_Mul x y)))))
(assert (forall ((x Term) (y Term)) (! (= (_Div x y) (box (div (unbox x) (unbox y)))) :pattern ((_Div x y)))))
(assert (forall ((x Int)) (! (= x (unbox (box x))) :pattern ((box x)))))
(assert (forall ((x Term)) (! (= x (box (unbox x))) :pattern ((box (unbox x))))))

(echo "")
(echo "----------- tests with +, *, div --------")

(push)
(echo "(3 * (3 * a)) / 3 = a * 3")
(assert (not (= (div (* 3 (* 3 a)) 3) (* a 3))))
(check-sat)
(pop)

(push)
(echo "((3 * 3) * a) / 3 = a * 3")
(assert (not (= (div (* (* 3 3) a) 3) (* a 3))))
(check-sat)
(pop)

(push)
(echo "t = 3 ==> (t * (t * a)) / t = a * t")
(assert (not (= (div (* t (* t a)) t) (* a t))))
(check-sat)
(pop)

(push)
(echo "t = 3 ==> ((t * t) * a) / t = a * t")
(assert (not (= (div (* (* t t) a) t) (* a t))))
(check-sat)
(pop)

(push)
(echo "a * b = b * a")
(assert (not (= (* a b) (* b a))))
(check-sat)
(pop)

(push)
(echo "a * (b * c) = (a * b) * c")
(assert (not (= (* a (* b c)) (* (* a b) c))))
(check-sat)
(pop)

(push)
(echo "a * (b + c) = (a * b) + (a * c)")
(assert (not (= (* a (+ b c)) (+ (* a b) (* a c)))))
(check-sat)
(pop)

(push)
(echo "a * (b + c) = (c * a) + (a * b)")
(assert (not (= (* a (+ b c)) (+ (* c a) (* a b)))))
(check-sat)
(pop)

(push)
(echo "f(a) * (b + c) = (c * f(a)) + (f(a) * b)")
(assert (not (= (* (f a) (+ b c)) (+ (* c (f a)) (* (f a) b)))))
(check-sat)
(pop)

(push)
(echo "a = z ==> a * b = z * b")
(assert (not (= (* a b) (* z b))))
(check-sat)
(pop)

(push)
(echo "a = z ==> a * (b + c) = (c * a) + (z * b)")
(assert (not (= (* a (+ b c)) (+ (* c a) (* z b)))))
(check-sat)
(pop)

(echo "")
(echo "----------- tests with +, _mul, _div --------")

(push)
(echo "(3 * (3 * a)) / 3 = a * 3")
(assert (not (= (_div (_mul 3 (_mul 3 a)) 3) (_mul a 3))))
(check-sat)
(pop)

(push)
(echo "((3 * 3) * a) / 3 = a * 3")
(assert (not (= (_div (_mul (_mul 3 3) a) 3) (_mul a 3))))
(check-sat)
(pop)

(push)
(echo "t = 3 ==> (t * (t * a)) / t = a * t")
(assert (not (= (_div (_mul t (_mul t a)) t) (_mul a t))))
(check-sat)
(pop)

(push)
(echo "t = 3 ==> ((t * t) * a) / t = a * t")
(assert (not (= (_div (_mul (_mul t t) a) t) (_mul a t))))
(check-sat)
(pop)

(push)
(echo "a * b = b * a")
(assert (not (= (_mul a b) (_mul b a))))
(check-sat)
(pop)

(push)
(echo "a * (b * c) = (a * b) * c")
(assert (not (= (_mul a (_mul b c)) (_mul (_mul a b) c))))
(check-sat)
(pop)

(push)
(echo "a * (b + c) = (a * b) + (a * c)")
(assert (not (= (_mul a (+ b c)) (+ (_mul a b) (_mul a c)))))
(check-sat)
(pop)

(push)
(echo "a * (b + c) = (c * a) + (a * b)")
(assert (not (= (_mul a (+ b c)) (+ (_mul c a) (_mul a b)))))
(check-sat)
(pop)

(push)
(echo "f(a) * (b + c) = (c * f(a)) + (f(a) * b)")
(assert (not (= (_mul (f a) (+ b c)) (+ (_mul c (f a)) (_mul (f a) b)))))
(check-sat)
(pop)

(push)
(echo "a = z ==> a * b = z * b")
(assert (not (= (_mul a b) (_mul z b))))
(check-sat)
(pop)

(push)
(echo "a = z ==> a * (b + c) = (c * a) + (z * b)")
(assert (not (= (_mul a (+ b c)) (+ (_mul c a) (_mul z b)))))
(check-sat)
(pop)

(echo "")
(echo "----------- tests with _add, _mul, _div --------")

(push)
(echo "(3 * (3 * a)) / 3 = a * 3")
(assert (not (= (_div (_mul 3 (_mul 3 a)) 3) (_mul a 3))))
(check-sat)
(pop)

(push)
(echo "((3 * 3) * a) / 3 = a * 3")
(assert (not (= (_div (_mul (_mul 3 3) a) 3) (_mul a 3))))
(check-sat)
(pop)

(push)
(echo "t = 3 ==> (t * (t * a)) / t = a * t")
(assert (not (= (_div (_mul t (_mul t a)) t) (_mul a t))))
(check-sat)
(pop)

(push)
(echo "t = 3 ==> ((t * t) * a) / t = a * t")
(assert (not (= (_div (_mul (_mul t t) a) t) (_mul a t))))
(check-sat)
(pop)

(push)
(echo "a * b = b * a")
(assert (not (= (_mul a b) (_mul b a))))
(check-sat)
(pop)

(push)
(echo "a * (b * c) = (a * b) * c")
(assert (not (= (_mul a (_mul b c)) (_mul (_mul a b) c))))
(check-sat)
(pop)

(push)
(echo "a * (b + c) = (a * b) + (a * c)")
(assert (not (= (_mul a (_add b c)) (_add (_mul a b) (_mul a c)))))
(check-sat)
(pop)

(push)
(echo "a * (b + c) = (c * a) + (a * b)")
(assert (not (= (_mul a (_add b c)) (_add (_mul c a) (_mul a b)))))
(check-sat)
(pop)

(push)
(echo "f(a) * (b + c) = (c * f(a)) + (f(a) * b)")
(assert (not (= (_mul (f a) (_add b c)) (_add (_mul c (f a)) (_mul (f a) b)))))
(check-sat)
(pop)

(push)
(echo "a = z ==> a * b = z * b")
(assert (not (= (_mul a b) (_mul z b))))
(check-sat)
(pop)

(push)
(echo "a = z ==> a * (b + c) = (c * a) + (z * b)")
(assert (not (= (_mul a (_add b c)) (_add (_mul c a) (_mul z b)))))
(check-sat)
(pop)

(echo "")
(echo "----------- tests with _Add, _Mul, _Div --------")

(push)
(echo "(3 * (3 * A)) / 3 = A * 3")
(assert (not (= (_Div (_Mul (box 3) (_Mul (box 3) A)) (box 3)) (_Mul A (box 3)))))
(check-sat)
(pop)

(push)
(echo "((3 * 3) * A) / 3 = A * 3")
(assert (not (= (_Div (_Mul (_Mul (box 3) (box 3)) A) (box 3)) (_Mul A (box 3)))))
(check-sat)
(pop)

(push)
(echo "T = 3 ==> (T * (T * A)) / T = A * T")
(assert (not (= (_Div (_Mul T (_Mul T A)) T) (_Mul A T))))
(check-sat)
(pop)

(push)
(echo "T = 3 ==> ((T * T) * A) / T = A * T")
(assert (not (= (_Div (_Mul (_Mul T T) A) T) (_Mul A T))))
(check-sat)
(pop)

(push)
(echo "A * B = B * A")
(assert (not (= (_Mul A B) (_Mul B A))))
(check-sat)
(pop)

(push)
(echo "A * (B * C) = (A * B) * C")
(assert (not (= (_Mul A (_Mul B C)) (_Mul (_Mul A B) C))))
(check-sat)
(pop)

(push)
(echo "A * (B + C) = (A * B) + (A * C)")
(assert (not (= (_Mul A (_Add B C)) (_Add (_Mul A B) (_Mul A C)))))
(check-sat)
(pop)

(push)
(echo "A * (B + C) = (C * A) + (A * B)")
(assert (not (= (_Mul A (_Add B C)) (_Add (_Mul C A) (_Mul A B)))))
(check-sat)
(pop)

(push)
(echo "F(A) * (B + C) = (C * F(A)) + (F(A) * B)")
(assert (not (= (_Mul (F A) (_Add B C)) (_Add (_Mul C (F A)) (_Mul (F A) B)))))
(check-sat)
(pop)

(push)
(echo "A = Z ==> A * B = Z * B")
(assert (not (= (_Mul A B) (_Mul Z B))))
(check-sat)
(pop)

(push)
(echo "A = Z ==> A * (B + C) = (C * A) + (Z * B)")
(assert (not (= (_Mul A (_Add B C)) (_Add (_Mul C A) (_Mul Z B)))))
(check-sat)
(pop)
